T, A:Type, P:(AT), i:Id, k:Knd.
Normal(A)
 Normal(T)
 ((isrcv(k))  (i = destination(lnk(k))))
 ((locl("a") = k))
 (trigger1{trigger:ut2, a:ut2, x:ut2}(T; A; P; i; k)  Realizer) 

latex

Definitions	ff, eq_atom$n(x;y), Atom2Deq, t.1, a = b, P & Q, , P  Q, P  Q, tt, eqof(d), if b then t else f fi , Top, x. t(x), IdDeq, trigger1{$trigger:ut2, $a:ut2, $x:ut2}(T; A; P; i; k), t  T, "$x", A, b, P  Q, Knd, Id, x:A. B(x), False, x(s), State(ds)
Lemmas	IdLnk wf, normal-type wf, lnk wf, ldst wf, isrcv wf, locl wf, Knd wf, not wf, bool wf, Rpre wf, false wf, assert-eq-id, eq id wf, fpf-single-dom, top wf, fpf-dom wf, assert wf, not functionality wrt iff, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, Id wf, fpf-single wf, R-base-recognize wf, Rlist wf